; EXPECT: sat
(set-option :incremental false)
(set-option :sets-ext true)
(set-logic ALL)
(declare-sort Atom 0)
(declare-fun C32 () (Relation Atom))
(declare-fun C2 () (Relation Atom))
(declare-fun C4 () (Relation Atom))
(declare-fun ATOM_UNIV () (Relation Atom))
(declare-fun V1 () Atom)
(assert (= C32 (set.inter (set.complement C2) (set.complement C4))))
(assert (set.member (tuple V1) (set.complement C32)))
(assert (= ATOM_UNIV (as set.universe (Relation Atom))))
(assert (set.member (tuple V1) ATOM_UNIV))
(assert (set.member (tuple V1) (set.complement C2)))
(check-sat)
